1. Technical Field
The present invention relates to computer program verification and analysis, and more particularly to a system and method capable of efficient analysis of threads with bounded lock chains.
2. Description of the Related Art
Multi-threading is a standard way of exploiting parallelism among different components of a computer system. As a result, the use of concurrent multi-threaded programs is becoming pervasive. Examples include operating systems, databases, embedded systems (cell phones, multimedia consumer products), etc.
Existing techniques for testing and verifying sequential programs are inadequate in handling concurrent programs, largely due to the many possible interleavings between concurrent modules, leading to subtle and hard-to-debug errors. This has led to an interest in developing efficient and scalable methods for analyzing concurrent programs.
Conventional methods for restricting the set of interleavings to be explored includes Partial Order Reduction (POR), Thread-Modular Model Checking and the Acquisition History Method. A main idea behind POR is to partition all interleavings of the given program into classes based on the partial order they induce on shared objects. Then, it suffices to explore only one interleaving per partial order.
The Thread-Modular Model Checking technique is based on over-approximating the behavior of other threads when analyzing the behavior of a given thread in a concurrent program. These over-approximations are hard to generate both manually and automatically as the problem of model checking is theoretically unsolvable.
The acquisition history method works only for concurrent programs with nested locks and involves tracking lock acquisition patterns for nested locks via acquisition histories. To decide reachability, a consistency check is then performed on the acquisition histories.